(declare-const x Float32)
(declare-const y Float32)
(declare-const z Float32)
(define-const x2 Float64 ((_ to_fp 11 53) RNE x))
(define-const y2 Float64 ((_ to_fp 11 53) RNE y))
(define-const z2 Float64 ((_ to_fp 11 53) RNE z))
(define-const r Float32 (fp.fma RNE x y z))
(define-const r2 Float32 ((_ to_fp 8 24) RNE (fp.add RNE (fp.mul RNE x2 y2) z2)))
(assert (not (= r r2)))
(check-sat)
